Problem:
 r(r(x1)) -> s(r(x1))
 r(s(x1)) -> s(r(x1))
 r(n(x1)) -> s(r(x1))
 r(b(x1)) -> u(s(b(x1)))
 r(u(x1)) -> u(r(x1))
 s(u(x1)) -> u(s(x1))
 n(u(x1)) -> u(n(x1))
 t(r(u(x1))) -> t(c(r(x1)))
 t(s(u(x1))) -> t(c(r(x1)))
 t(n(u(x1))) -> t(c(r(x1)))
 c(u(x1)) -> u(c(x1))
 c(s(x1)) -> s(c(x1))
 c(r(x1)) -> r(c(x1))
 c(n(x1)) -> n(c(x1))
 c(n(x1)) -> n(x1)

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {7,6,5,4,3}
   transitions:
    u1(52) -> 53*
    u1(42) -> 43*
    u1(32) -> 33*
    u1(14) -> 15*
    c1(54) -> 55*
    c1(51) -> 52*
    n1(44) -> 45*
    n1(41) -> 42*
    s1(34) -> 35*
    s1(31) -> 32*
    s1(13) -> 14*
    r1(22) -> 23*
    r1(24) -> 25*
    b1(12) -> 13*
    b1(16) -> 17*
    r0(2) -> 3*
    r0(1) -> 3*
    s0(2) -> 4*
    s0(1) -> 4*
    n0(2) -> 5*
    n0(1) -> 5*
    b0(2) -> 1*
    b0(1) -> 1*
    u0(2) -> 2*
    u0(1) -> 2*
    t0(2) -> 6*
    t0(1) -> 6*
    c0(2) -> 7*
    c0(1) -> 7*
    1 -> 54,44,34,24,16
    2 -> 51,41,31,22,12
    15 -> 23,25,14,3
    17 -> 13*
    23 -> 14*
    25 -> 14*
    33 -> 32,4
    35 -> 32*
    43 -> 42,5
    45 -> 42*
    53 -> 52,7
    55 -> 52*
  problem:
   
  Qed